import os
import simsym
import symtypes
import errno
import model
import signal
import ptypes
import ProcessTable
import ProcessQueue
import Lock
import Context
import CURRENTPROCESS

IntArray = symtypes.tdict(simsym.SInt, ptypes.APREF)

class Semaphore(simsym.tstruct(
		waiters		= ProcessQueue.ProcessQueue,
		scnt		= simsym.SInt,
		initval		= simsym.SInt,
		ptab		= ProcessTable.ProcessTable,
		sched		= CURRENTPROCESS.CURRENTPROCESS,
		ctxt		= Context.Context,
		lck		= Lock.Lock
		)):
	def _declare_assumptions(self, assume):
		super(Semaphore, self)._declare_assumptions(assume)
	
	@model.methodwrap(
		iv		= simsym.SInt,
		pt		= ProcessTable.ProcessTable,
		sch		= ptypes.LowLevelScheduler,
		ct		= Context.Context,
		lk		= Lock.Lock)
	def INIT(self, iv, pt, sch, ct, lk):
		self.initval = iv
		self.scnt = iv
		self.ptab = pt
		self.sched = sch
		self.ctxt = ct
		self.lck = lk
		self.waiters.INIT
	
	@model.methodwrap()
	def NegativeSemaCount(self):
		return self.scnt < 0
	
	@model.methodwrap()
	def NonPositiveSemaCount(self):
		return self.scnt <= 0
	
	@model.methodwrap()
	def IncSemaCount(self):
		self.scnt = self.scnt + 1
	
	@model.methodwrap()
	def DecSemaCount(self):
		self.scnt = self.scnt - 1
	
	@model.methodwrap()
	def Wait(self):
		self.lck.Lock
		self.DecSemaCount
		if (self.NegativeSemaCount):
			self.waiters.Enqueue(ptypes.currentp)
			cpd = self.ptab.DescrOfProcess(ptypes.currentp)
			cpd.SetProcessStatusToWaiting
			self.ctxt.SwapOut
			self.sched.MakeUnready(ptypes.currentp)
			self.sched.RunNextProcess
		else:
			self.sched.ContinueCurrent
		self.lck.Unlock
	
	@model.methodwrap()
	def Signal(self):
		self.lck.Lock
		self.IncSemaCount
		if (self.NonPositiveSemaCount):
			cand = self.waiters.RemoveFirst
			cpd = self.ptab.DescrOfProcess(cand)
			cpd.SetProcessStatusToReady
			self.sched.MakeReady(cand)
		else:
			self.sched.ContinueCurrent

		self.lck.Unlock

model_class = Semaphore
